#pragma once
#include "PDTCodeGraph.h"
#include "PDTFunction.h"
#include "PDTCondition.h"
#include "PDTBehavior.h"
#include "PDTType.h"
#include "PDTNumVar.h"
#include "PDTNumConst.h"

class PDTSpecCheck
{
private:
	PDTCodeGraph *CG;

public:
	PDTSpecCheck(PDTCodeGraph *CGtoSet) : CG(CGtoSet) {
	}

	//In all functions, funcName is the name of the function to SpecCheck

	//Build the ranges of all inputs and all outputs based on the given GOOD behaviors
	//The ranges are returned in a vector parallel to the variables vector
    void buildGoodRanges(PDTFunctionDec & functionDec, 
        PDTBehaviors& behaviors,
        string funcName, 
        vector <PDTIntRange*> & ranges, 
        vector <PDTVar*> & variables);

	//Build the ranges of all inputs and all outputs based on the given BAD behaviors
	//The ranges are returned in a vector parallel to the variables vector
    void buildBadRanges(PDTFunctionDec & functionDec,
        PDTBehaviors & behaviors,
        string funcName, 
        vector <PDTIntRange*> & ranges, 
        vector <PDTVar*> & variables);

	//Build the ranges of all inputs and all outputs based on the given ALL behaviors
	//The ranges are returned in a vector parallel to the variables vector
    void buildAllRanges(PDTFunctionDec& functionDec,
        PDTBehaviors & behaviors,
        const string & funcName, 
        vector <PDTIntRange*> &ranges, 
        vector <PDTVar*> & variables);

	//Check the pre and post conditions using specific good behavior numbered behaviorID
    void checkGood(PDTFunctionDec& functionDec,
        PDTPreCondition& preCondition,
        PDTPostCondition& postCondition,
        PDTBehaviors& behaviors,
        const string & funcName, 
        int behaviorID);

	//Check the pre and post conditions using specific bad behavior numbered behaviorID
    void checkBad(PDTFunctionDec& functionDec,
        PDTPreCondition& preCondition,
        PDTPostCondition& postCondition,
        PDTBehaviors& behaviors,
        const string & funcName, 
        int behaviorID);

	//Check the pre and post conditions using all good behaviors
    void checkAllGood(PDTFunctionDec& functionDec,
        PDTPreCondition& preCondition,
        PDTPostCondition& postCondition,
        PDTBehaviors& behaviors,
        const string & funcName);

	//Check the pre and post conditions using all bad behaviors
    void checkAllBad(PDTFunctionDec& functionDec,
        PDTPreCondition& preCondition,
        PDTPostCondition& postCondition,
        PDTBehaviors& behaviors,
        const string & funcName);

	//CHeck the pre and post conditions using all behaviors
    void checkAll(PDTFunctionDec& functionDec,
        PDTPreCondition& preCondition,
        PDTPostCondition& postCondition,
        PDTBehaviors& behaviors,
        const string & funcName);

	//If S is included, this function finds O, O', pre and post for each and based on tables1, 2 and 3, it returns the result
	void checkWithCode( PDTFunctionDec& functionDec,
        PDTPreCondition& preCondition,
        PDTPostCondition& postCondition,
        PDTBehaviors& behaviors,
        const string & funcName);

	//Retrieve S: the list of statements contained in the program code
	PDTListOfStatements& getFunctionCode(PDTFunctionDec& functionDec);

	//Compare two PDTNode nodes: used to compare outputs in checkWithCode function
	bool nValueEqual(PDTNode* node1, PDTNode* node2);

	//This function uses the previous functions in a smart way based on the given input
	void check(string funcName, string spec);
};
